COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	\input macro[1,mps]
C00012 ENDMK
C⊗;
\input macro[1,mps]
\magnification\magstephalf
\baselineskip 14pt
\def\m{\mathop{\rm m}\nolimits}
\def\mgu{\mathop{\rm mgu}\nolimits}
\leftline{\sevenrm A01.Tex[1,rwf]\today}
\leftline{\copyright\sevenrm Robert W. Floyd, January 4, 1989}
\leftline{\sevenrm Unpublished draft}
\noindent{\bf Most General Unification}

\bigskip
A {\it substitution} is a function ${\sigma}$ (typically represented by a
lowercase Greek letter in postfix notation) on wffs, homomorphic for
functions (including constants): $f(e↓1, e↓2)\sigma = f(e↓1 \sigma,
e↓2 \sigma)$.  A substitution is completely determined by its restriction
${\overline\sigma}$ to variables, and may be represented by
$\{\langle x, x\sigma\rangle \mid x\sigma\not= x\in V\}$.  Like all
homomorphisms, substitutions are closed under associative composition.
The identity function $\iota$ is a substitution, and $\iota\sigma = \sigma
= \sigma\iota$.  Substitutions form a monoid under composition, with identity
$\iota$.

We say $\tau$ is {\it less general} than (or a descendant of) $\sigma$,
$\tau\prec\sigma$ or $\sigma\succ\tau$, if there is a $\rho$ for which
$\tau = \sigma\rho$.  This relation is reflexive and transitive, with
maximal element $\iota$ (not unique).  There is an associated equivalence,
$\tau\sim\sigma$ if $\tau\prec\sigma\prec\tau$; reflexive, symmetric, and
transitive.

We say wff $e↓1$ is an {\it instance} of $e↓2$, $e↓1\prec e↓2$, if $e↓1 = e↓2
\sigma$.  If $\sigma\prec\tau$, $e\sigma\prec e\tau$.  Again there is an
associated equivalence $e↓1 \sim e↓2$, if $e↓1\prec e↓2\prec e↓1$.

A {\it unifier} of $e↓1, e↓2$ is a substitution $\sigma$ for which
$e↓1\sigma = e↓2\sigma$.  If $\sigma$ is a unifier of $e↓1, e↓2$, then
so is $\tau\prec\sigma$.  A substitution unifies $e↓1, e↓2$ and unifies
$e↓3, e↓4$ iff it unifies $f(e↓1, e↓3), f(e↓2, e↓4)$.
\medskip
\noindent{\bf To unify {$A, B$}} 

We show by induction that there are two possibilities:
\medskip
\item{$\bullet$} Nothing unifies $A, B$

\item{$\bullet$} There is a substitution $\mu$ that unifies $A, B$ and every
unifier of $A, B$ is less general than $\mu$, (i.e., of the form $\mu\rho$)
\medskip
In the latter case, every descendant of $\mu$ unifies $A, B$, so the unifiers of
$A, B$ are exactly the descendants of $\mu$, which is called a {\it most general
unifier} of $A, B$, $\mgu (A, B)$.

By cases, omitting obvious symmetric cases:
\medskip
\item{$\bullet$} $A = x = B$.  Let $\mu = \iota$ (identity).  Every substitution
$\rho$ is a descendant $\iota\rho$ of $\iota$, and $A\iota = B\iota$.

\item{$\bullet$}$A = x$, $x$ occurs in $B$, $x \not= B$.  Then under any
substitution $\sigma$, $A\sigma$ is shorter than $B\sigma$, so no unifier exists.

\item{$\bullet$}  $A = x$, $x$ does not occur in $B$.  
Define $\overline\mu$ by $x{\overline\mu} = B$, $y{\overline\mu} = y$ if $x \not=
y \in V$.  Then $\mu$ unifies $A, B$.  If $\rho$ is any unifier,
$$\eqalign{x\mu\rho & = B\rho =  A\rho = x\rho\cr
y\mu\rho & = y\rho  \quad\hbox{for } y \hbox{ a variable} \not= x, \cr}$$

so $\overline{\rho} = \overline{\mu\rho},  \rho = \mu\rho, \mu\succ\rho.$

\item{$\bullet$} $A = f(A↓1), B = g(B↓1)$, or $A = f(A↓1, A↓2), B = g(B↓1, B↓2)$.
There is no unifier.

\item{$\bullet$} $A = f(A↓1), B = f(B↓1)$.  The unifiers of $A, B$ are those of
$A↓1, B↓1$, so $\mu =$ $\mgu (A↓1, B↓1)$.

\item{$\bullet$} $A = f(A↓1, A↓2)$, $B = f(B↓1, B↓2)$.
\medskip
\noindent Let $\mu↓1 =$ $\mgu (A↓1, B↓1)$ if it exists; if $\mu↓1$ exists, let
$\mu↓2 = \mgu (A↓2\mu↓1, B↓2\mu↓1)$.  Then let $\mu = \mu↓1\mu↓2$;
$$\eqalign{A↓1\mu &= A↓1\mu↓1\mu↓2 = B↓1\mu↓1\mu↓2 = B↓1\mu\cr
A↓2\mu &= A↓2\mu↓1\mu↓2 = B↓2\mu↓1\mu↓2 = B↓2\mu\cr
f(A↓1, A↓2) \mu &= f(B↓1, B↓2)\mu\cr}$$
so $\mu$ is a unifier of $A, B$.  If $\rho$ is any unifier of $A,B$, then $\rho$ 
is a unifier of $A↓1, B↓1$ and of $A↓2, B↓2$, $\mu↓1$ exists, and $\rho \prec
\mu↓1$.  Say $\rho = \mu↓1\sigma$, so $A↓2\mu↓1\sigma = A↓2\rho = B↓2\rho =
B↓2\mu↓1\sigma$, $\sigma$ unifies $A↓2\mu↓1$, $B↓2\mu↓1$.  Then 
$\mu↓2$ exists, $\sigma \prec\mu↓2$, and $\rho = \mu↓1\sigma\prec\mu↓1\mu↓2
= \mu$; $\mu$ is the most general unifier of $A, B$.

To make the induction valid requires well-ordering the argument pairs
$\{A, B\}$ appropriately.  Order first by the number of distinct variables, then
by total length.  Add to the induction hypothesis, that every most general unifier
as defined above either is the identity or eliminates some variables of
$\{A, B\}$.  The argument can be stated:  let $\{A, B\}$ be an argument pair of 
minimum number of variables, and minimum length for pairs with that number of
variables, for which there is doubt about the theorem, etc.

If $\mu↓1$ and $\mu↓2$ are two most general unifiers of $A, B$ then
$\mu↓1 > \mu↓2$ and $\mu↓2 > \mu↓1$, so $\mu↓1 \sim\mu↓2$.

It may be convenient in practice to define another function $\m(\nu, A, B)$ to 
be the most general unifier of $A, B$ that is a descendant of $\nu$.  Then $\mgu
(A, B) =\, \m (\iota, A, B)$, and $\m(\nu, A, B) = \nu \mgu (A\nu, B\nu)$.

The definition of $\m$ includes
$$\eqalign{\m(\nu, x, x) & = \nu\cr
\m (\nu, x, B) & = \nu \m(\iota, x \nu, B\nu)\qquad 
(\nu \not= \iota)\cr
\m(\nu, f(A↓1, A↓2), f(B↓1, B↓2)) & = \m(\m
(\nu, A↓1. B↓1), A↓2, B↓2)\cr
\m(\iota, x, B) & = \dots, \hbox {etc.}\cr}$$

The results above readily generalize to multiple unifications, as suggested
by unification of $f(e↓1, e↓3)$, $f(e↓2, e↓4)$.

(Note to mathematicians)  Like the set of all substitutions, 
the set of unifiers of $e↓1, e↓2$ has a
maximal element, and consists of its descendants.  This is reminiscent of
principal ideal rings.  Suggest anything?  What is the analogue of the GCD?

\noindent [RWF:  When complete, send to Doug Smith, Cordell, NN, Mike G.]
\bye